COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	know[f81,jmc]		draft of paper on knowledge
C00015 00003	Translation of Modal Axioms into First Order Logic
C00019 ENDMK
C⊗;
know[f81,jmc]		draft of paper on knowledge

FORMALISMS FOR REASONING ABOUT KNOWLEDGE


	Intelligent programs must reason about their knowledge, about
the knowledge of people and other programs and about the presence of
information in documents and computer files.  It is important to be
able to conclude that someone knows a fact or the value of a term but
also that someone does not know these things.  Programs must also
reason about beliefs which are not necessarily true.
It is also necessary to reason about changes in knowledge with time
as a consequence of learning and forgetting.

	This paper discusses several formalisms for representing facts about
knowledge.  None of them is proposed as "the ultimate truth about knowledge".
The innovations are in the areas of providing ways of expressing facts
about the totality of a person's knowledge, proving non-knowledge,
describing the effects of learning, and a concept of joint knowledge
needed for expressing the effects of events that occur in the presence
of several people.


Introduction

	The requirement for formalizing facts about knowledge is one
that AI (artificial intelligence) shares with philosophy.  However,
it seems that AI imposes a different research
strategy than is customary in philosophy even though AI has much
to learn from the formalisms proposed by philosophers and logicians.
Philsophers attempt to devise formalisms that express the facts
about (say) knowledge.  Other philosophers then find examples
which the given formalism doesn't treat adequately, and the search
is on for a new formalism.  To my knowledge, philosophers never use
the formalisms discussed to express substantial bodies of knowledge.

	AI work must use the formalisms in
programs and for expressing all the facts it can about some domain.
AI cannot affort to discard a formalism just because
a counterexample can be found provided it is useful for some problems
unless a more comprehensive formalism is available that is
just as convenient.

	In fact, it may be that the search for an ultimate formalism
for knowledge is just as doomed as the search for an ultimate system
of axioms for arithmetic and for the same reasons.  Given a formalism
for representing facts about knowledge, some facts can be found that
are unrepresentable in this formalism.  In the concluding section
of this paper, we will elaborate this, and we will offer some suggetions
for mitigating its ill effects.  These suggestions involve non-monotonic
reasoning.

	Some of the formalisms we discuss are forms of modal logic, while
others use first order languages in which propositions and individual
concepts are objects of the logic and modalities are expressed by
logically ordinary functions and predicates.  The first order formalisms
can express facts (mainly about non-knowledge) that we have not been
able to express in the modal formalisms.  Thus our slogan seems to be,
"Modality yes, modal logic no".


Two puzzles

	Much of our work has involved on two puzzles about knowledge and
its change over time.  The first is the puzzle of the three wise men
usually told as follows:

	"A certain king wishes to determine which of his three
wise men is the wisest.  He
arranges them in a circle so that they can see and hear each other and tells
them that he will put a white or black spot on each of their foreheads
but that at least one spot will be white.  In fact all three spots
are white.  He then offers his favor to the one who will first tell
him the color of his spot.  After a while, the wisest announces
that his spot his white.  How does he know?"

	The intended solution is that the wisest reasons that if
his spot were black, the second would see a black and a white and
would reason that if his spot were black, the third would have seen
two black spot and reasoned from the king's announcement that his
spot was white.

	If the above form of the puzzle is interpreted literally,
the third wise man must reason about how fast his colleagues reason.
We are not prepared to do this, and the usual informal solutions of
the problem don't do it either.  Therefore, it is simpler treat a version
of the puzzle in which the king asks the wise men in turn whether
they know the colors of their spots and the first two answer "no",
and the third answers "yes".  We formalize the state of knowledge
after the third wise man is asked the question.

	In this form the modal formalism is adequate to represent
the facts stated so that the fact that the third wise man knows the color
of his spot can be deduced.  This version is unfair, since
the third wise man has the advantage.  A symmetric version
of the puzzle is the following:

	%2"A certain king wishes to test his three wise men.  He
arranges them in a circle so that they can see and hear each other and tells
them that he will put a white or black spot on each of their foreheads
but that at least one spot will be white.  In fact all three spots
are white.  He then repeatedly asks them, "Do you know the cclor of
your spot".  What do they answer?"%1

	The solution is that they answer, %2"No"%1, the first two
times the question is asked and answer %2"Yes"%1 thereafter.

	In order to formalize it properly, we need to consider
knowledge as a function of time.  This can be done with
yet another formalism that involves time as a parameter
and permits deducing that each wise man knows the color of his
spot after the third time the king asks.  The formalism can't
express knowledge about time but merely different states of
knowledge at different times.
If it is stated that the answer is "no" the first two times, then
the puzzle can be formalized in a modal logic.  If this must
be deduced by the solver, thus making the problem harder, we
have not been able to do it modally but have had to use a
direct formalization of the Kripke accessability relation
between possible worlds.

	The following puzzle of the unfaithful wives turns out
to be a variant of the wise men puzzle.

	"The Caliph of Baghdad decrees that there is too much
infidelity in Baghdad and that every man who determines that
his wife is unfaithful should behead her in the market place at
noon of the following day.  The inhabitants of Baghdad are great
gossips and everyone knows of all affairs except that no-one would
ever tell a man that his own wife is unfaithful.  As it happens,
there are forty unfaithful wives.  Nothing happens for thirty-nine
days, but on the fortieth day all the unfaithful wives are beheaded.
What was the reasoning of the men who beheaded their wives?"

	The second major puzzle is that of Mr. S and Mr. P.

	Two numbers ⊗m and ⊗n are chosen such that 2_≤_m_≤_n_≤_99.
Mr. S is told their sum and Mr. P is told their product.  The following
dialogue ensues:

Mr. P:	I don't know the numbers.

Mr. S:	I knew you didn't know them.  I don't know either.

Mr. P:	Now I know the numbers.

Mr. S:	Now I know them too.

In view of the above dialogue, what are the numbers?"


A modal formalism

	This modal propositional logic of knowledge represents the
sentence "S knows p" by the formula  S*p.  Otherwise the language is
that of propositional logic.  We want to avoid the any rule corresponding
to necessitation in modal logic, because we often want to assert
propositions that are true but not known.  Therefore we include a
special person called "any fool" and denoted by 0.  Thus 0*p may
be read "any fool knows p".  The sole rule of inference is modus
ponens and the following are taken as axiom schemata.

	S*p ⊃ p

	0*(S*p ⊃ p)

	0*(0*p ⊃ 0*S*p)

	0*(S*p ∧ S*(p ⊃ q) ⊃ S*q)

	0*π for any tautology π

We call the above system KT3.  KT4 has the additional axiom

	0*(S*p ⊃ S*S*p),

and KT5 has the axiom

	0*(¬S*p ⊃ S*¬S*p).
Translation of Modal Axioms into First Order Logic

	Ordinary first order logic does not allow modal operators that
take propositions into proposition and such that the truth value of the
composite proposition is not a function of the truth values of
the component propositions.  Nevertheless, the modal knowledge system
described in the preceding section can be translated in the following
way.

	As before, we have S*p  denoting "S knows p", but now  S*p
is a term rather than a sentence; call it a propositional term.  In
order to assert a propositional term  p  we must write  true(p).
Propositional terms are propositionally combined by propositional
functions  and,  or, not, implies and equiv corresponding to
the propositional operators ∧, ∨, ¬, ⊃
and ≡ respectively.  These functions satisfy the axioms

	∀p q.true(p and q) ≡ true(p) ∧ true(q)

	∀p q.true(p or q) ≡ true(p) ∨ true(q)

	∀p q.true(p implies q) ≡ true(p) ⊃ true(q)

	∀p.true(not p) ≡ ¬true(p)

	∀p q.true(p equiv q) ≡ (true(p) ≡ true(q))

[We may remark that using the above as rewrite rules combined with
a tautology checker in an interactive theorem prover like Weyhrauch's
FOL or Ketonen's EKL permits any "tautologous" formula of this
language to be verified in a single step.]

	Our previous set of axiom schemata then become

	∀S p.true(S * p implies p)

	∀S p.true(0*(S*p implies p))

	∀S p.true(0*(0*p implies 0*S*p))

	∀S p q.true(0*(S*p and S*(p implies q) implies S*q)))

	The last schema becomes

	∀p.tautology(p) ⊃ true(0*p),

This last requires formalizing the notion of tautology.  If this isn't
convenient, then it can be replaced by asserting that "any fool" knows
a set of axioms for propositional calculus.  The following
three axioms will suffice.

	∀p q.true 0*(p implies (q implies p))

	∀p q r.true 0*((r implies (p implies q)) and (r implies p) implies (r implies q))

	∀p.true 0*(not not p implies p)

and the introspective axioms become

	∀S p.true(0*(S*p implies S*S*p))

and

	∀S p.true(0*(not S*p implies S*(not S*p))).